Admissible behaviors: This is essentially faireness type settings. PAT will automatically enable the suitable fairness options (not supported in Orc Module) for the user according to the model and the property selected. Notice that all fairness options are disabled except for LTL assertions. For more information, please refer to section 4.1 Fairness and [SUNLDP09]. 

• No Fairness: By default, this option is selected. In this setting, no fairness assumption is applied to the system (even for event-annotated fairness).
• Process Level Weak Fairness: Selecting this option means that for every process in the system, if it is eventually always enabled, it must eventually always occur. This option is similar to the one in SPIN. This option is only enabled, if the system to be checked is an interleave or parallel composition.
• Process Level Strong Local Fairness: Selecting this option means that for every process in the system, if it is always eventually enabled, it must eventually always occur. This option is only enabled, if the system to be checked is an interleave or parallel composition.
• Strong Global Fairness: Selecting this option means to apply strong global fairness to the system, i.e., each transition must eventually always occur if it is always eventually enabled.

Verification Engine: For all safety properties (e.g. deadlockfree, reachability, refinement relation), in explicit model checking, PAT performs Depth-First-Search to explore the state space for the purpose of fast verification. However, if there is any counterexample, it is desired to have the shortest trace to find the bug quickly. Hence, we provide this option to user such that PAT performs Breadth-First-Search to find the shortest witness trace. Similarly symbolic model checking provides 3 search engines. These search engines are both breadth first search with different directions.

• Symbolic Model Checking using BDD with Forward Search Strategy: check the safety property starting from the initial state, and go forward to check whether bad states can be reachable from the inital state.
• Symbolic Model Checking using BDD with Backward Search Strategy: check the safety property starting from the bad states and go backward to check whether the initial state is reachable.
• Symbolic Model Checking using BDD with Forward-Backward Search Strategy: check the safefy property starting from both initial state and bad states. At each step, it will go forward from the initial state direction and go backward from the bad state direction.

 Some other choices are provided for specific properties such as Strongly Connected Component Based Search (explicit model checking) and Symbolic Model Checking using BDD for liveness properties. Please refer to Assertion page in the each module's subsection of Language Reference in Section 3.

Time Out: This option allows you to limit the running time. If it is set to 0, then system can run as long as it got a result or out of memory. If it is set to a number greater than 0 then system will stop in due time if it hasn't got any result. 

Generate Witness Trace: This option is provided to get the model checking result without the counter example if exists.

MODES:

Click Mode:    Use this mode to verify the properties, you have to manually click the assertions one by one and choose the additional options described above.

Note: Multiple assertion selection is supported from the version 3.4.

Batch Mode: Use this mode, you can get all the properties of a batch of model files verified with certain choices of options in one time. The whole verification result will be written into an output file you defined. These results can also be converted to excel files by clicking the button "Generate Excel Report".

To use this function, you can click the Tools tab in PAT's Editor, and select Verification (Batch Mode).